Step of Proof: band_ff_simp
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
band
ff
simp
:
u
:
. (
u
ff) = ff
latex
by
InteriorProof
((((UnivCD)
CollapseTHENM (BoolEval))
)
CollapseTHEN ((Auto_aux (first_nat
CollapseTHEN ((Aut
1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))
latex
C
.
Definitions
t
T
Lemmas
bool
wf
,
bfalse
wf
origin